Nuprl Lemma : lnk-inv_wf 0,22

l:IdLnk. lnk-inv(l IdLnk 
latex


DefinitionsId, t  T, x:AB(x), xt(x), 2of(t), 1of(t), lnk-inv(l), IdLnk
Lemmaspi1 wf, pi2 wf, Id wf

origin